(set-logic NRA)
(set-option :model_validate true)
(set-option :model true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r5 Real)
(declare-const v19 Bool)
(assert v12)
(declare-const r6 Real)
(assert v6)
(assert v15)
(declare-const v20 Bool)
(assert (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15))
(assert (or v11 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) v20 v6 (=> v12 v2) v1 v18 v13 v6))
(declare-const r7 Real)
(declare-const v21 Bool)
(declare-const v22 Bool)
(assert v22)
(declare-const v23 Bool)
(assert v10)
(assert (< (+ r4 r4 70123529 7222330864) 22899.00 r7 70123529))
(declare-const v24 Bool)
(declare-const r8 Real)
(declare-const v25 Bool)
(declare-const v26 Bool)
(assert (=> (or v11 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) v20 v6 (=> v12 v2) v1 v18 v13 v6) v1))
(declare-const v27 Bool)
(declare-const r9 Real)
(declare-const v28 Bool)
(declare-const v29 Bool)
(declare-const r10 Real)
(assert (not (= v0 v0 v7 (or v11 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) v20 v6 (=> v12 v2) v1 v18 v13 v6) v21 (< r3 r6) (or v11 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) v20 v6 (=> v12 v2) v1 v18 v13 v6))))
(declare-const r11 Real)
(assert (exists ((q0 Bool) (q1 Real)) (=> (= q1 22899.00 q1 0.8499893) (distinct (>= 749 r7 (- (/ r7 7222330864))) q0 v16 q0 v21 q0 q0 q0 (and v6 v11 (and v23 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) (distinct v11 v7 (distinct r4 749) v13 v20 v19 v8)) v11 v20 (>= 749 r7 (- (/ r7 7222330864)))) q0))))
(assert (not v20))
(declare-const v30 Bool)
(assert (or (not (= v0 v0 v7 (or v11 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) v20 v6 (=> v12 v2) v1 v18 v13 v6) v21 (< r3 r6) (or v11 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) v20 v6 (=> v12 v2) v1 v18 v13 v6))) v30 (>= 749 r7 (- (/ r7 7222330864)))))
(assert (forall ((q2 Real)) v26))
(declare-const v31 Bool)
(declare-const v32 Bool)
(assert v19)
(declare-const r12 Real)
(assert (forall ((q3 Bool) (q4 Real) (q5 Bool) (q6 Real)) (not (and q3 (xor (not v20) v4 v18 (and v23 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) (distinct v11 v7 (distinct r4 749) v13 v20 v19 v8)) v13 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) (= r7 749) (or v11 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) v20 v6 (=> v12 v2) v1 v18 v13 v6) v21 (< r3 r6) v28) (distinct r4 749) q5 (not (= v0 v0 v7 (or v11 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) v20 v6 (=> v12 v2) v1 v18 v13 v6) v21 (< r3 r6) (or v11 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) v20 v6 (=> v12 v2) v1 v18 v13 v6))) q3 v21 v21 (< r3 r6) q5 q3))))
(assert (or (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) (distinct r6 r7 723974) (<= (- 7222330864) 7222330864 84776279 (/ (* 0.8499893 749) 84776279) 70123529)))
(declare-const r13 Real)
(assert (exists ((q7 Bool) (q8 Bool) (q9 Real)) (not (not q7))))
(declare-const v33 Bool)
(assert (= (< r3 r6) v31))
(assert (exists ((q10 Bool) (q11 Real)) (not (<= q11 q11 (- r9)))))
(assert v22)
(assert (=> v25 v31))
(assert (xor (=> v2 (or v11 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) v20 v6 (=> v12 v2) v1 v18 v13 v6)) (distinct r6 r7 723974) v6 (>= 749 r7 (- (/ r7 7222330864))) (=> (or v11 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) v20 v6 (=> v12 v2) v1 v18 v13 v6) v1) v7 v33 v32))
(assert (forall ((q12 Real) (q13 Bool) (q14 Real)) (= r7 749)))
(assert v2)
(declare-const v34 Bool)
(declare-const r14 Real)
(declare-const v35 Bool)
(assert (forall ((q15 Real) (q16 Bool) (q17 Bool)) v19))
(declare-const r15 Real)
(assert v1)
(declare-const v36 Bool)
(assert (or (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) (distinct r6 r7 723974) (<= (- 7222330864) 7222330864 84776279 (/ (* 0.8499893 749) 84776279) 70123529)))
(assert (= (=> (or v11 (or (distinct r4 749) v10 (distinct r4 749) v16 v6 v1 v15) v20 v6 (=> v12 v2) v1 v18 v13 v6) v1) v14 (distinct r4 749)))
(declare-const r16 Real)
(assert (= (< r3 r6) v31))
(declare-const v37 Bool)
(declare-const r17 Real)
(assert v0)
(declare-const v38 Bool)
(assert (or v23 (distinct r4 749) v4 (not v1) v18 (not v25) (distinct r10 22899.00 (- 703310516.0) (/ (* 0.8499893 749) 84776279)) (<= (- 7222330864) 7222330864 84776279 (/ (* 0.8499893 749) 84776279) 70123529) (>= (- 7222330864) (- (/ r7 7222330864)) r8) v11 (not v1)))
(declare-const r18 Real)
(assert (< r3 r6))
(check-sat-using solve-eqs)
